Nuprl Definition : ring_non_triv
13,42
postcript
pdf
r
0 == 1
0
|
r
|
latex
clarification:
r
0 == 1
r
0
r
|
r
|
latex
Up
rings
1
Wellformedness Lemmas
ring
non
triv
wf
Definitions
a
b
T
,
|
r
|
,
1
,
0
origin
0 == 1 0 
|r|
0 == 1r 0r |r| 0 == 1 0 |r|
0 == 1r 0r |r| b T